@InProceedings{StoneHar00,
  author =       "Christopher A. Stone and Robert Harper",
  title =        "Deciding Type Equivalence in a Language with Singleton
                 Kinds",
  booktitle =    "Conference Record of {POPL}'00: The 27th {ACM}
                 {SIGPLAN}-{SIGACT} Symposium on Principles of
                 Programming Languages",
  address =      "Boston, Massachusetts",
  month =        jan # " 19--21,",
  year =         "2000",
  pages =        "214--227",
}

@Article{Shao:2002:TSC,
  author =       "Zhong Shao and Bratin Saha and Valery Trifonov and
                 Nikolaos Papaspyrou",
  title =        "A type system for certified binaries",
  journal =      "ACM SIG{\-}PLAN Notices",
  volume =       "37",
  number =       "1",
  pages =        "217--232",
  month =        jan,
  year =         "2002",
  CODEN =        "SINODQ",
  ISSN =         "0362-1340",
  bibdate =      "Thu May 15 12:22:58 MDT 2003",
  acknowledgement = ack-nhfb,
  annote =       "Proceedings of the 29th ACM SIGPLAN-SIGACT symposium
                 on Principles of Programming Languages (POPL'02).",
}


@InProceedings{PasalicLingerGpce,
  author =   "Emir Pasalic and Nathan Linger",
  title =    "Meta-Programming with Typed Object-Language Representations",
  booktitle = "Generative Programming and Component Engineering (GPCE'04)",
  city = "Vancouver B.C.",
  month = "October",
  year = "2004",
  note = "LNCS volume 3286",
  pages = "136 - 167"
  }

@InProceedings{SheardLogFrWks04,
  author =   "Tim Sheard and Emir Pasalic",
  title =    "Meta-programming with Built-in Type Equality",
  booktitle = "Logical Frameworks and Meta-Languages workshop",
  city = "Cork, Ireland",
  month = "July",
  year = "2004",
  note = "Available at:\\ {\small {\tt http://cs-www.cs.yale.edu/homes/carsten/lfm04/}}"
  }
  
@Article{Sheard:2004:LF,
  author =       "Tim Sheard",
  title =        "Languages of the future",
  journal =      "Onward Track, OOPSLA'04. Reprinted in: ACM SIG{\-}PLAN Notices, Dec 2004",
  volume =       "39",
  number =       "10",
  pages =        "116--119",
  month =        oct,
  year =         "2004",
  CODEN =        "SINODQ",
  ISSN =         "0362-1340",
  bibdate =      "Thu Dec 2 05:49:56 MST 2004",
  acknowledgement = ack-nhfb,
}  

@Misc{SheardLinger,
   author = "Tim Sheard and Nathan Linger",
   title = "Programming with Static Invariants in Omega",
   month = "September",
   year = "2004",
   note = "Available from:\\{\small {\tt http://www.cs.pdx.edu/\verb+~+sheard/ }}"
   }

@TechReport{SheardHookLinger,
   author = "Tim Sheard and Jim Hook and Nathan Linger",
   title = "{GADT}s + Extensible Kinds = Dependent Programming",
   institution = "Portland State University",
   month = "April",
   year = "2005",
   note = "Available from:\\{\small {\tt http://www.cs.pdx.edu/\verb+~+sheard/}}"
   }
  
@InProceedings{Sheard02,
  author =       "T. Sheard and S. Peyton-Jones",
  title =        "Template meta-programming for {Haskell}.",
  booktitle =    "Proc. of the workshop on Haskell",
  pages =        "1--16",
  publisher =    "ACM",
  year =         "2002",
  keywords =     "wShop, templates, functional programming, FP, zz1002,
                 compile-time, skeleton, program patterns,
                 metaprogramming, type, types, polytypic, macro,
                 in-line, inline, expansion",
  abstract =     "{"}...extension to the purely functional programming
                 language Haskell that supports compile-time
                 meta-programming. The purpose of the system is to
                 support the algorithmic construction of programs at
                 compile-time. The ability to generate code at compile
                 time allows the programmer to implement such features
                 as polytypic programs, macro-like expansion, user
                 directed optimization (such as inlining), and the
                 generation of supporting data structures and functions
                 from existing data structures and functions. Our design
                 is being implemented in the Glasgow Haskell Compiler,
                 ghc.{"} [http://doi.acm.org/10.1145/581690.581691
                 (paper)][10/'02]
                 http://www.amazon.com/exec/obidos/ISBN=1581136056/fourwheeldriveinA/
                 . [Also see: generic Haskell (etc.)]
                 [http://www.haskell.org/th/ (haskell.org/th/)][2/'04]",
}


@Misc{SheardStrict,
   author = "Tim Sheard",
   title = "A Pure Language with Default Strict Evaluation Order and Explicit Laziness",
   month = "August",
   year = "2003",
   note = "Available from:\\{\small {\tt http://www.cs.pdx.edu/\verb+~+sheard/ }}"
   }  
 
@Article{TS00,
author =       "Walid Taha and Tim Sheard",
title =        "{MetaML}:  Multi-Stage Programming with Explicit 
                Annotations",
journal =      "Theoretical Computer Science",
year =         "2000",
volume =       248,
number =       "1-2",
}

@Article{Sheard:1999:UMS,
  author =       "T. Sheard",
  title =        "Using {MetaML}: {A} Staged Programming Language",
  journal =      "Lecture Notes in Computer Science",
  volume =       "1608",
  pages =        "207--239",
  year =         "1999",
  coden =        "LNCSD9",
  ISSN =         "0302-9743",
  bibdate =      "Mon Sep 13 16:57:02 MDT 1999",
  acknowledgement = ack-nhfb,
}

@TechReport{RankN,
  author =       {Simon Peyton Jones and Mark Shields},
  title =        {Practical type inference for arbitrary-rank types},
  institution =  {Microsoft Research},
  year =         {2003},
  OPTkey =       {},
  OPTtype =      {},
  OPTnumber =    {},
  OPTaddress =   {},
  month =        {"December"},
  note =         {{\scriptsize \verb+http://research.microsoft.com/Users/simonpj/papers/putting/index.htm+}},
  OPTannote =    {Available from \cite{ogi-tr-site}}
}

@Article{gabbay-pitts-02,
  author =       "Murdoch J. Gabbay and Andrew M. Pitts",
  title =        "A New Approach to Abstract Syntax with Variable
                 Binding",
  journal =      "Formal Aspects of Computing",
  year =         "2002",
  volume =       "13",
  number =       "3--5",
  pages =        "341--363",
  month =        jul,
}


@InProceedings{CurryHoward,
  author =   "Tim Sheard",
  title =    "Putting {Curry}-{Howard} to Work",
  booktitle = "Proceedings of the ACM SIGPLAN 2005 Haskell Workshop",
  year = "2005",
  city = "Tallin, Estonia",
  pages = "74--85"
  }

@Article{Antoy:2005:ESF,
  author =      "Sergio Antoy",
  title =       "Evaluation strategies for functional logic
                 programming",
  journal =     "Journal of Symbolic Computation",
  volume =      "40",
  number =      "1",
  pages =       "875--903",
  month =       jul,
  year =        "2005",
  CODEN =       "JSYCEH",
  ISSN =        "0747-7171",
  bibdate =     "Tue Jul 5 17:59:15 MDT 2005",
  bibsource =   "http://www.sciencedirect.com/science/journal/07477171",
  acknowledgement = "Nelson H. F. Beebe, University of Utah, Department
                 of Mathematics, 110 LCB, 155 S 1400 E RM 233, Salt Lake
                 City, UT 84112-0090, USA, Tel: +1 801 581 5254, FAX: +1
                 801 581 4148, e-mail: \path|beebe@math.utah.edu|,
                 \path|beebe@acm.org|, \path|beebe@computer.org|
                 (Internet), URL:
                 \path|http://www.math.utah.edu/~beebe/|",
}

@phdThesis{XiThesis,
  author =      "Hongwei Xi",
  title =       "Dependent Types in Practical Programming",
  degree =      "Ph. D.",
  institution = "Carnegie Mellon University",
  school =  "Carnegie Mellon University",
  year =        "1997"
}

@InProceedings{Xi:1999:DTP,
  author =       "Hongwei Xi and Frank Pfenning",
  title =        "Dependent types in practical programming",
  editor =       "{ACM}",
  booktitle =    "{POPL} '99. Proceedings of the 26th {ACM}
                 {SIGPLAN-SIGACT} on Principles of programming
                 languages, January 20--22, 1999, San Antonio, {TX}",
  publisher =    "ACM Press",
  address =      "New York, NY, USA",
  ISBN =         "1-58113-095-3",
  series =       "ACM SIG{\-}PLAN Notices",
  pages =        "214--227",
  year =         "1999",
  bibdate =      "Mon May 3 12:58:58 MDT 1999",
  URL =          "http://www.acm.org:80/pubs/citations/proceedings/plan/292540/p214-xi/",
  acknowledgement = ack-nhfb,
  subject =      "{\bf F.4.1} Theory of Computation, MATHEMATICAL LOGIC
                 AND FORMAL LANGUAGES, Mathematical Logic. {\bf D.3.2}
                 Software, PROGRAMMING LANGUAGES, Language
                 Classifications, ML. {\bf D.1.1} Software, PROGRAMMING
                 TECHNIQUES, Applicative (Functional) Programming. {\bf
                 D.3.3} Software, PROGRAMMING LANGUAGES, Language
                 Constructs and Features, Polymorphism.",
}

@Article{Cardelli-Wegner85,
  key =         "Cardelli \& Wegner",
  author =      "Luca Cardelli and Peter Wegner",
  title =       "On Understanding Types, Data Abstraction and
                 Polymorphism",
  journal =     "ACM Computing Surveys",
  volume =      "17",
  number =      "4",
  month =       dec,
  year =        "1985",
  pages =       "471--522",
  annote =      "Model of typed, polymorphic programming languages.
                 Existential and bounded quantification. Lambda calculus
                 based model of type systems. The language Fun. 44
                 references.",
}

@InProceedings{conf/alp/Antoy92,
  title =       "Definitional Trees",
  author =      "Sergio Antoy",
  year =        "1992",
  bibdate =     "2002-02-04",
  bibsource =   "DBLP,
                 http://dblp.uni-trier.de/db/conf/alp/alp92.html#Antoy92",
  booktitle =   "ALP",
  pages =       "143--157",
}

@InProceedings{HinzeHaskellWorkshop02,
  author =       {Hinze, Ralf and Cheney, James},
  title =        {A Lightweight Implementation of Generics and Dynamics},
  booktitle =    {Proceedings of the ACM SIGPLAN 2002 Haskell Workshop},
  OPTcrossref =  {},
  OPTkey =       {},
  pages =        {90-104},
  year =         {2002},
  editor =       {Manuel Chakravarty},
  OPTvolume =    {},
  OPTnumber =    {},
  OPTseries =    {},
  OPTaddress =   {},
  month =        {October},
  organization = {ACM SIGPLAN},
  OPTpublisher = {},
  OPTnote =      {},
  OPTannote =    {}
}

@MISC{Hanus06Curry,
author       = "Hanus (ed.), M.",
title        = "Curry: An Integrated Functional Logic Language (Vers.\ 0.8.2)",
year         = {March 28, 2006},
howpublished = "Available at \verb+http://www.informatik.uni-kiel.de/~curry+"
} 


@Article{journals/jflp/HanusS99,
  title =       "An Abstract Machine for Curry and Its Concurrent
                 Implementation in Java",
  author =      "Michael Hanus and Ramin Sadre",
  journal =     "Journal of Functional and Logic Programming",
  year =        "1999",
  number =      "Special Issue 1",
  volume =      "1999",
  bibdate =     "2002-01-03",
  bibsource =   "DBLP,
                 http://dblp.uni-trier.de/db/journals/jflp/jflp1999.html#HanusS99",
}

 @techreport{Playing,
 title = "Playing with Types",
 author = "Tim Sheard",
 institution = "Portland State University",
 year = "2005",
 note = {{\tt http://www.cs.pdx.edu/\verb+~+sheard}}
 }


@Article{Coquand:1994:IDT,
  author =       "T. Coquand and P. Dybjer",
  title =        "Inductive Definitions and Type Theory: an Introduction.
                 (Preliminary Version)",
  journal =      "Lecture Notes in Computer Science",
  volume =       "880",
  pages =        "60--76",
  year =         "1994",
  CODEN =        "LNCSD9",
  ISSN =         "0302-9743",
  bibdate =      "Wed Sep 15 10:01:31 MDT 1999",
  acknowledgement = ack-nhfb,
  keywords =     "software technology; theoretical computer science;
                 computer; science",
}



@Article{Dybjer:1999:FAI,
  author =       "P. Dybjer and A. Setzer",
  title =        "A Finite Axiomatization of Inductive-Recursive
                 Definitions",
  journal =      "Lecture Notes in Computer Science",
  volume =       "1581",
  pages =        "129--146",
  year =         "1999",
  CODEN =        "LNCSD9",
  ISSN =         "0302-9743",
  bibdate =      "Tue Sep 14 06:09:05 MDT 1999",
  acknowledgement = ack-nhfb,
  keywords =     "lambda calculi; TLCA; typed lambda calculi",
}

@Article{JACM::HarperHP1993,
  title =        "A Framework for Defining Logics",
  author =       "Robert Harper and Furio Honsell and Gordon Plotkin",
  area =         "Logic in Computer Science",
  pages =        "143--184",
  journal =      "Journal of the ACM",
  month =        jan,
  year =         "1993",
  volume =       "40",
  number =       "1",
  references =   "\cite{IC::Avron1991} \cite{IC::CoquandH1988}
                 \cite{LICS::MendlerA1988} \cite{JACM::Robinson1965}",
}

@InProceedings{Pfenning91lf,
  author =       "Frank Pfenning",
  title =        "Logic Programming in the {LF} Logical Framework",
  booktitle =    "Logical Frameworks",
  editor =       "G\'{e}rard Huet and Gordon Plotkin",
  publisher =    "Cambridge University Press",
  address =      "Cambridge, England",
  pages =        "149--181",
  year =         "1991",
  fullurldvi =   "http://www.cs.cmu.edu/~fp/papers/lfproc91.dvi.gz",
  fullurlps =    "http://www.cs.cmu.edu/~fp/papers/lfproc91.ps.gz",
  keywords =     "LF, Elf",
}


@InProceedings{CADE99*202,
  author =       {Frank Pfenning and Carsten Sch\"{u}rmann},
  title =        "System Description: Twelf --- {A} Meta-Logical
                 Framework for Deductive Systems",
  pages =        "202--206",
  ISBN =         "3-540-66222-7",
  editor =       "Harald Ganzinger",
  booktitle =    "Proceedings of the 16th International Conference on
                 Automated Deduction ({CADE}-16)",
  month =        jul # "~7--10,",
  series =       "LNAI",
  volume =       1632,
  publisher =    "Springer-Verlag",
  address =      "Berlin",
  year =         1999,
} 


@Misc{oai:CiteSeerPSU:339817,
  title =        "Equality proofs in {Cayenne}",
  author =       "Lennart Augustsson",
  year =         "2000",
  month =        jul # "~11",
  abstract =     ". We introduce a simple syntactical extension to
                 Cayenne to make equality proofs readable. 1
                 Introduction Equality proofs are important for
                 functional programs, since they are encouraged by
                 equational reasoning. Unfortunately, type theory style
                 equational proofs are tedious and look very ugly. Let
                 us illustrate this with an example. We wish to prove
                 that list append is associative. The function has the
                 following denition: Nil ++ ys = ys (x : xs) ++ ys = x :
                 (xs ++ ys) Now we want to establish that (xs++ys)++zs =
                 xs++(ys++zs). With normal notation we do this with an
                 inductive proof 1 as follows. Base case: (Nil++ys)++zs
                 = by rst clause of ++ = ys++zs = by rst clause of ++,
                 reversed = Nil++(ys++zs) Inductive step:
                 ((x:xs)++ys)++zs = by second clause of ++ =
                 (x:(xs++ys))++zs = by second clause of ++ =
                 x:((xs++ys)++zs) = by induction hypothesis =
                 x:(xs++(ys++zs)) = by second clause of ++, reversed =
                 (x:xs)++(ys++zs) Now compare this to the same proof in
                 type theory style. W...",
  citeseer-isreferencedby = "oai:CiteSeerPSU:291358;
                 oai:CiteSeerPSU:373381; oai:CiteSeerPSU:156676;
                 oai:CiteSeerPSU:310596; oai:CiteSeerPSU:42657;
                 oai:CiteSeerPSU:375952; oai:CiteSeerPSU:108132;
                 oai:CiteSeerPSU:300895; oai:CiteSeerPSU:375033;
                 oai:CiteSeerPSU:332599",
  annote =       "The Pennsylvania State University CiteSeer Archives",
  language =     "en",
  oai =          "oai:CiteSeerPSU:339817",
  rights =       "unrestricted",
  subject =      "Lennart Augustsson Equality proofs in {Cayenne}",
  note =         "\\ \verb+http://www.cs.chalmers.se/~augustss/cayenne/eqproof.ps+",
}



@Article{Augustsson:1999:CLD,
  author =       "Lennart Augustsson",
  title =        "{Cayenne} --- a Language with Dependent Types",
  journal =      "ACM SIG{\-}PLAN Notices",
  volume =       "34",
  number =       "1",
  pages =        "239--250",
  month =        jan,
  year =         "1999",
  CODEN =        "SINODQ",
  ISSN =         "0362-1340",
  bibdate =      "Sun Dec 14 09:17:56 MST 2003",
  acknowledgement = ack-nhfb,
  affiliation =  "Chalmers University",
}


@TechReport{LuoPollack92,
  author =       "Zhaohui Luo and Robert Pollack",
  title =        "{LEGO} Proof Development System: User's Manual",
  institution =  "LFCS, Computer Science Dept., University of
                 Edinburgh",
  year =         "1992",
  number =       "ECS-LFCS-92-211",
  address =      "The King's Buildings, Edinburgh EH9 3JZ",
  month =        may,
  note =         "Updated version",
  classification = "LF",
}

@Misc{oai:CiteSeerPSU:38734,
  title =        "The {ALF} proof editor",
  author =       "Bengt Nordstrom",
  year =         "1996",
  month =        mar # "~20",
  abstract =     "Alf is an interactive proof editor. It is based on the
                 idea that to prove a mathematical theorem is to build a
                 proof object for the theorem. The proof object is
                 directly manipulated on the screen, different
                 manipulations correspond to different steps in the
                 proof. The language we use is Martin-Lof's monomorphic
                 type theory. This is a small functional programming
                 language with dependent types. The language is open in
                 the sense that it is easy to introduce new inductively
                 defined sets. A proof is represented as a mathematical
                 object and a proposition is identified with the set of
                 its proof objects. Background During the years we have
                 learned that there is no such thing as {"}the logic of
                 programming{"}. Different kinds of programs require
                 different kind of reasoning. Programs are manipulating
                 different kinds of objects, and it would be very
                 awkward to code these objects into a fixed set of
                 objects. Objects have their own logic, it is for
                 instance very different to reason about ongoing
                 proce...",
  citeseer-isreferencedby = "oai:CiteSeerPSU:2648;
                 oai:CiteSeerPSU:176010; oai:CiteSeerPSU:53007;
                 oai:CiteSeerPSU:234809; oai:CiteSeerPSU:224766",
  annote =       "The Pennsylvania State University CiteSeer Archives",
  language =     "en",
  oai =          "oai:CiteSeerPSU:38734",
  rights =       "unrestricted",
  subject =      "Bengt Nordstrom The ALF proof editor",
  note =          "\\ \verb+ftp://ftp.cs.chalmers.se/pub/users/ilya/FMC/alfintro.ps.gz+",
}


@InProceedings{epigram,
  author =   "Connor McBride",
  title =    "Epigram: Practical Programming with Dependent Types",
  booktitle = "Notes from the 5th International Summer School on 
              Advanced Functional Programming ",
  city = "Tartu, Estonia",
  month = "August",
  year = "2004",
  note = "Available at:\\ {\scriptsize {\tt http://www.dur.ac.uk/CARG/epigram/epigram-afpnotes.pdf }}"
  }

@Misc{oai:CiteSeerPSU:495376,
  title =        "First-Order Unification by Structural Recursion",
  author =       "Conor Mcbride",
  year =         "2001",
  month =        aug # "~16",
  abstract =     "First-order unification algorithms (Robinson, 1965)
                 are traditionally implemented via general recursion,
                 with separate proofs for partial correctness and
                 termination. The latter tends to involve counting the
                 number of unsolved variables and showing that this
                 total decreases each time a substitution enlarges the
                 terms. There are many such proofs in the literature,
                 for example, (Manna \& Waldinger, 1981; Paulson, 1985;
                 Coen, 1992; Rouyer, 1992; Jaume, 1997; Bove, 1999).",
  citeseer-isreferencedby = "oai:CiteSeerPSU:77059;
                 oai:CiteSeerPSU:437063; oai:CiteSeerPSU:345366",
  annote =       "The Pennsylvania State University CiteSeer Archives",
  language =     "en",
  oai =          "oai:CiteSeerPSU:495376",
  rights =       "unrestricted",
  subject =      "Conor Mcbride First-Order Unification by Structural
                 Recursion",
  URL =          "http://citeseer.ist.psu.edu/495376.html;
                 http://www.dur.ac.uk/~dcs1ctm/unify.ps",
}

 



@Misc{Agda,
  title =        "Agda is a system for incrementally developing proofs and programs",
  author =       "Catarina Coquand",
  note = "Web page describing AGDA: 
   \\ {\small {\tt http://www.cs.chalmers.se/\verb+~+catarina/agda/ }}"
 }


@InProceedings{Rogue,
  author =   "Aaron Stump",
  title =    "Imperative {LF} Meta-Programming",
  booktitle = "Logical Frameworks and Meta-Languages workshop",
  city = "Cork, Ireland",
  month = "July",
  year = "2004",
  note = "Available at:\\ {\small {\tt http://cs-www.cs.yale.edu/homes/carsten/lfm04/}}"
  }
  

@Manual{COQ74,
  title =        {The Coq Proof Assistant Reference Manual, Version 7.4},
  OPTkey =       {},
  author =       {{The Coq Development Team}},
  organization = {INRIA},
  OPTaddress =   {},
  OPTedition =   {},
  OPTmonth =     {},
  year =         {2003},
  note =         {\verb+http://pauillac.inria.fr/coq/doc/main.html+},
  OPTannote =    {}
}



@InCollection{Paulson90lacs,
  author =       "Lawrence C. Paulson",
  title =        "{Isabelle}: The Next 700 Theorem Provers",
  booktitle =    "Logic and Computer Science",
  editor =       "P. Odifreddi",
  publisher =    "Academic Press",
  year =         "1990",
  pages =        "361--386",
  urldvi =       
"http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz",
  keywords =     "Isabelle",
}


@techreport{RSP1,
  author =   "Edwin Westbrook and Aaron Stump and Ian Wehrman",
  title =    "A Language-based Approach to Functionally Correct INperative Programming",
  year = "2005",
  institution = "Washington University in St. Louis",
  note = "Available at:\\ {\small {\tt http://cl.cse.wustl.edu/}}"
  }

@Article{Xi:1998:EAB,
  author =       "Hongwei Xi and Frank Pfenning",
  title =        "Eliminating Array Bound Checking Through Dependent
                 Types",
  journal =      "ACM SIG{\-}PLAN Notices",
  volume =       "33",
  number =       "5",
  pages =        "249--257",
  month =        may,
  year =         "1998",
  CODEN =        "SINODQ",
  ISBN =         "0-89791-987-4",
  ISSN =         "0362-1340",
  bibdate =      "Sun Dec 14 09:17:47 MST 2003",
  URL =          "http://www.acm.org:80/pubs/citations/proceedings/pldi/277650/p249-xi/",
  acknowledgement = ack-nhfb,
  annote =       "Published as part of the Proceedings of PLDI'98.",
  keywords =     "algorithms; experimentation; languages; performance",
  subject =      "{\bf F.3.3} Theory of Computation, LOGICS AND MEANINGS
                 OF PROGRAMS, Studies of Program Constructs, Type
                 structure. {\bf D.3.2} Software, PROGRAMMING LANGUAGES,
                 Language Classifications, Standard ML. {\bf D.3.3}
                 Software, PROGRAMMING LANGUAGES, Language Constructs
                 and Features, Data types and structures.",
}

@InProceedings{ATS2004,
  author =   "Hongwei Xi",
  title =    "Applied Type Systems (extended abstract)",
  booktitle = "In post-workshop proceedings of TYPES 2003",
  pages = "394 -- 408",
  year = "2004",
  note = "Springer-Verlag LNCS 3085"
  }


@InProceedings{ATS2005,
  author =   "Chiyan Chen and Hongwei Xi",
  title =    "Combining Programming with Theorem Proving",
  booktitle = "ICFP 2005",
  year = "2005",
  note = "\verb+http://www.cs.bu.edu/~hwxi/+"
  }

@InProceedings{Davies97,
  author =       "Rowan Davies",
  title =        "A refinement-type checker for {S}tandard {ML}",
  booktitle =    "International Conference on Algebraic Methodology and
                 Software Technology",
  series =       "Lecture Notes in Computer Science",
  publisher =    "Springer-Verlag",
  volume =       "1349",
  year =         "1997",
  fullissn =     "0302-9743",
}


@InProceedings{CheXi05,
  author =      "Chen and Xi",
  title =       "Combining Programming with Theorem Proving",
  booktitle =    "Proceedings of the 2005 ACM/SIGPLAN International Conference on Functional Programming (ICFP'05)",
  city = "Tallin, Estonia",
  month = "September",
  pages = "66 -- 77",
  year =        "2005",
}

@Article{FridlenderI00,
  title =       "Do we need dependent types?",
  author =      "Daniel Fridlender and Mia Indrika",
  journal =     "J. Funct. Program",
  year =        "2000",
  number =      "4",
  volume =      "10",
  bibdate =     "2004-03-19",
  bibsource =   "DBLP,
                 http://dblp.uni-trier.de/db/journals/jfp/jfp10.html#FridlenderI00",
  pages =       "409--415",
}

@Article{peyton-jones:haskell98,
  author =      "Simon {Peyton Jones}",
  title =       "Special Issue: {H}askell 98 Language and Libraries",
  journal =     "Journal of Functional Programming",
  year =        "2003",
  volume =      "13",
  month =       jan,
}
